from XSY.Set.Interval import *
from XSY.Base import *

def isClockDifferenceDict(ob):
   '''check if ob is a clock difference dictionary'''
   if isinstance(ob, dict):
      for k in ob:
         if not (isinstance(k, tuple) and len(k)==2):
            return False
      return True
   else:
      return False

def isClockDict(ob):
   '''check if ob is a clock dictionary'''
   if isinstance(ob, dict):
      return True
   else:
      return False

def isInfinity(sigma):
   if isnumeric(sigma):
      return sigma == float('inf')
   elif isinstance(sigma, Interval):
      return sigma.infinity()
   elif isinstance(sigma, tuple):
      return sigma[0] == float('inf')
   else: 
      return False

class TID:
   '''
Clobk Difference Intervals are a set of intervals b(i,j) of clock difference for each pair of clocks i, j in the set of clocks C0=C \cup {0} where 0 is the dummy clock whose value is 0.

Here we use Python's 2-tuple structure for the clock pair (i,j), so cd(i,j) is simplified cd((i,j)).  Since cd(i,j)= -cd(j,i), we just record cd(i,j) where <i> i>j </i> for both of cd(i,j) and cd(j,i). For evaluating cd(j,i) for j>i, we will use -b(i,j). Since b(i,i)=0 for all i, we don't have to manage it. In addition, we ignore the clock i \in C if sigma(i)=[infty,infty] becase there is no way to get enabled like e(i) = sigma(i)  
   '''
   c0 = 0 # pure clock name
   inf_trim_out = False
   inv00 = Interval(0,0)
   key_repo = {}
   value_repo = {}

   def __init__(self):
      '''constructor'''
      self.cd = {} # mem alloc
      self.activeC_init = False
      self.C=set()
      self.C.add(TID.c0)
      self.activeC=set([TID.c0])  # c0 must be an element of activeC 


   def registerC(self, schedules):
      '''collect a list of active clock names, schedules is a dictionary (clockname, clockvalue)'''
      if self.activeC_init == False:
         self.activeC_init = True
         
         for k in schedules.keys():
            if isinstance(k, tuple):
               if k[1]== TID.c0 :
                  self.C.add(k[0])
                  if TID.inf_trim_out==False or not schedules[k].infinity(): # k[0] must be an active clock
                     self.activeC.add(k[0]) # add clock k[0]
            else:
               self.C.add(k)
               if TID.inf_trim_out==False or not schedules[k].infinity(): # k must be an active clock
                  self.activeC.add(k) # add clock k[0]

         #self.activeC.sort()
      #print 'activeC=', self.activeC

      return self.activeC

   def IsDegenerated(self):
      '''check if there exists only one actice clock that is TID.c0'''
      return len(self.activeC)==1 #and self.activeC[0] == TID.c0

   def set_cd(self, k,v):
      ''' set cd[k]=v using repository '''
      if k not in self.key_repo:
         self.key_repo[k]=k
      key = self.key_repo[k]

      if v not in self.value_repo:
         self.value_repo[v]=v
      value = self.value_repo[v]
      self.cd[key]=value

   def use_repo(self):
      '''use all memory from repository'''
      for k in self.cd:
         self.set_cd(k, self.cd[k])

   def make(self, clockdiff):
      '''make all active clocks including their difference'''
      if isClockDifferenceDict(clockdiff): 
         self.registerC(clockdiff)
         for i in self.C:
            for j in self.C:
               if i > j and (i,j) in clockdiff: # (i,j) is a 2-tuple
                  v = clockdiff[(i,j)]
                  #print "v=%s"%str(v)
                  self.cd[(i,j)]=Interval(v.l, v.u)
                  #self.set_cd((i,j), Interval(v.l, v.u))
         self.tighten()
         return self
      else:
         raise Exception("Invalide input of %s in %s"%(str(clockdiff), function_name()))

   def makeInvarient(self, schedules):
      '''make the TID as big as possible according to schedules'''
      if isClockDict(schedules):
         self.registerC(schedules)

         for i in self.C:
            if i == TID.c0: continue
            for j in self.C:
               if j == TID.c0: # b(i,TID.0)=b(i)
                  self.cd[(i,j)]= Interval(0, schedules[i].u)
                  #self.set_cd((i,j),Interval(0, schedules[i].u))
               elif i > j : # b(i,j) where i,j not eq TID.0
                  #print "v=%s"%str(v)
                  self.cd[(i,j)]= Interval(0,schedules[i].u) - Interval(0,schedules[j].u)
                  #self.set_cd((i,j), Interval(0,schedules[i].u) - Interval(0,schedules[j].u))
               else:
                  continue

         self.tighten()
         return self
      else:
         raise Exception("Invalide input of %s in %s"%(str(schedules), function_name()))

   def copy(self, ob):
      '''copy constructor'''
      if isinstance(ob, TID):
         #self.registerC(ob.cd) # copy activeclock names
         for c in ob.C: self.C.add(c)
         for c in ob.activeC: self.activeC.add(c)
         self.activeC_init = True
         for k in ob.cd :
            v = ob.cd[k]
            self.cd[k]=Interval(v.l, v.u)
            #self.set_cd(k, ob.cd[k])
         return self
      else:
         raise Exception("Invalide input of %s in %s"%(str(ob), function_name()))

   def makeZero(self, schedules):
      '''make the TID's all clocks zero as well as their differences''' 
      self.makeInvarient(schedules)

      for bk in self.cd.keys(): # for each key in b
         self.cd[bk] = TID.inv00
         #self.set_cd(bk,TID.inv00)

      return self

   def include(a, b):
      '''check if a includes b'''
      if isinstance(b, TID): 
         for k in a.cd.keys(): # for each key in b
            if a.isActiveKey(k):
               if a.cd[k].include(b.cd[k]) == False: return False
         return True
      else: 
         return False

   def checkH(self):
      '''check if hypothesis is true: it turns out failed -_-+'''
      m = 0;
      for k in self.cd:
         if k[0] != TID.c0:
            m = k[0]
            break

      result = True
      for i in self.C:
         if i == TID.c0: continue
         for j in self.C:
            if j == TID.c0: continue
            if i > j and j != m:
               print '---------------------------------'
               print 'b(%s,%s)=%s '%(i,j,self.b(i,j)) 
               print 'b(%s,%s)=%s '%(i,m,self.b(i,m)) 
               print 'b(%s,%s)=%s '%(j,m,self.b(j,m)) 
               print '---------------------------------'
               if self.b(i,j) != self.b(i,m) - self.b(j,m):
                  result = False
      return result

   def isActiveKey(self, (i,j)):
      return i in self.activeC and j in self.activeC

   def compare(a, b):
      for k in a.cd.keys():
         if a.isActiveKey(k):
            if a.cd[k] < b.cd[k]: return -1
            elif a.cd[k] > b.cd[k]: return 1
      return 0

   def __eq__(self, o): 
      '''equal to o'''
      return self.compare(o) == 0

   def __ne__(self, o):
      '''not equal to o'''
      return self.compare(o) != 0

   def __lt__(self, o):
      '''less than o'''
      return self.compare(o) < 0

   def __le__(self, o):
      '''less than or equal to o'''
      return self.compare(o) <= 0

   def __gt__(self, o):
      '''greater than o '''
      return self.compare(o) > 0

   def __ge__(self,o):
      '''greater than or equal to o'''
      return self.compare(o) >= 0

   def __hash__(self):
      total = 0
      for k in self.cd.keys():
         b = self.cd[k]
         if self.isActiveKey(k): 
            total += hash(b)
      return total

   def __str__(self):
      '''convert it into a string'''
      if self.IsDegenerated(): 
         return "."
      else:
         #print "#########################################################"
         #print 'activeC=',self.activeC
         s = ""
         first = True
         for k in self.cd.keys():
            if not self.isActiveKey(k): 
               #raw_input("%s,%s is not active."%(k[0],k[1]))
               continue

            #print k, " is active"
            b = self.cd[k]
            if first == False: s += ", "
            if k[1] == TID.c0: 
               s += str(b.l) + "<=" + str(k[0]) + "<=" + str(b.u)   
            else :
               s += str(b.l) + "<=" + str(k[0]) + "-" + str(k[1]) + "<=" + str(b.u)   
            first = False

         return s

   def intersect(self, ob):
      '''return new(self cap ob)'''
      clockZ = {}
      for ij in self.cd.keys():
          clockZ[ij]= self.cd[ij].intersect(ob.cd[ij])

      return TID().make(clockZ)
   
   def slide(self, schedules=None):
      '''make clocks' upperbounds go to infinity. But don't change clock differences.'''
      for ij in self.cd.keys(): 
         if ij[1] == TID.c0: # pure clock, not clock difference
            if schedules == None:
            	self.cd[ij] = Interval(self.cd[ij].l, float('inf'))
	    else:
	        self.cd[ij] = Interval(self.cd[ij].l, schedules[ij[0]].u) 
            #self.set_cd(ij, Interval(self.cd[ij].l, float('inf')))

   def slided(self):
      '''check if all clocks' upper bounds are infinity.'''
      for c in self.C: 
         if c == TID.c0: 
            continue 
         if self.b(c).u != float('inf'): 
            return False
      return True
  
   def valid(self):
      '''check if it is valid'''
      #if self.IsDegenerated():  # it is not invalid case. Don't activate it
      #   print 'Degenerated'
      #   return False

      for k in self.cd.keys():
         if self.cd[k].valid() == False:
            #print 'cd[%s]=%s'%(k,cd[k])
            return False

      return True

   def reset(self, resetC):
      '''reset all clocks in resetC and tighten'''
      for c in resetC:
         self.cd[(c,TID.c0)] = TID.inv00
         #self.set_cd((c,TID.c0), TID.inv00)

      for i in self.C:
         if i != TID.c0 : # a pure clock
            for j in self.C:
               if j != TID.c0 and i > j and (i in resetC or j in resetC):
                 self.cd[(i,j)]= self.b(i) - self.b(j)
                 #self.set_cd((i,j), self.b(i) - self.b(j))

      self.tighten()
   
   def b(self, i,j=c0):
      '''get the clock difference ci-cj interval. if cj=0, that is clock interval of ci.'''
      if i==j:
         return TID.inv00 

      if (i,j) in self.cd.keys(): 
         return self.cd[(i,j)]
      else:
         if (j,i) in self.cd.keys(): 
            return -self.cd[(j,i)]
         else:                    
            raise Exception("%s,%s index is not found in keys=%s!"%(i,j,self.cd.keys()))
   
   def tighten(self):
      '''trim out the trivial clocks, and tighten the non-trivial clock boundaries that based on 
      Floyd-Warshall shortest path algorithm.'''
      self.registerC(self.cd)

      for k in self.C:
         for i in self.C:
            for j in self.C:
               if i > j:
                  v = self.b(i,k) + self.b(k,j)
                  #print "b(%s,%s)+b(%s,%s)=%s"%(i,k,k,j, v)
                  bij = self.b(i,j)
                  key = (i,j)
                  self.cd[key] = Interval(max(bij.l, v.l), min(bij.u, v.u))
                  #self.set_cd(key, Interval(max(bij.l, v.l), min(bij.u, v.u)))

      #if self.checkH() == False:
      #   raise Exception("checkH is failed!")

      #return self

      #for i in self.C:
      #   for j in self.C:
      #      if i <= j:
      #         del self.cd[(i,j)]

# move r to left
   def Enabler(self, ci, sigma):
      '''make clock ci at sigma'''
      #raw_input("origin self: %s"%self)
      lb, ub = 0, 0
      if isnumeric(sigma):
         if sigma == float('inf'): 
            raise Exception("Enabler could not set to infinity!")
         else: 
            lb, ub = sigma, sigma 
      elif isinstance(sigma, Interval):
         if sigma.infinity(): 
            raise Exception("Enabler could not set to infinity!")
         else:
            lb, ub = sigma.l, sigma.u
      elif isinstance(sigma, tuple):
         if sigma[0] == float('inf'):
            raise Exception("Enabler could not set to infinity!")
         else:
            lb, ub = sigma[0], sigma[1]
      else: 
         raise Exception("%s's type %s is invalid !"%(sigma, type(sigma) ))
      self.cd[(ci, TID.c0)]= Interval(lb,ub)
      #self.set_cd((ci, TID.c0), Interval(lb,ub))
      #raw_input("after self: %s"%self)
      self.tighten() # finally tighten # not here but outside
      #raw_input("tighten self: %s"%self)

   def update_activeC(self, newactiveC):
      # add newly active c in self.activeC
      if TID.inf_trim_out:
         #for c in newactiveC:
         #   if c not in self.activeC: # c is newly active
         #      self.activeC.add(c)

         # remove c in self.activeC which is not active

         removingC = []
         for c in self.activeC:
            if c not in newactiveC:
               removingC.append(c)

         for c in removingC:
            self.activeC.remove(c)

   def successor(self, clockR, next_schedule):
      '''compute a TID (1) reseting self by clockR, (2) sliding it, and 
      (3) interseting with the TID constructed from ci=[t_s]
       Sliding(Resetting(varphi,clockR)) \cap Invariant(t_s)'''
      if isClockDict(next_schedule):
         next_scheduleCZ = TID()
         #next_scheduleCZ.makeInvarient(next_schedule) #Let's don't use this function 
         next_scheduleCZ.registerC(next_schedule) # use it instead of makeInvarient

         copy = TID().copy(self)
         #raw_input('self: %s, copy(self): %s'%(self, copy))

         #if self != copy: # time consuming 
            #raise Exception("copy failed at %s"%function_name())

         #print 'next_scheduleCZ=', next_scheduleCZ

         #print 'newC=',
         #for c in next_schedule:
         #   print 'c=',str(next_schedule[c])

         #print 'newC=',next_scheduleCZ.activeC
         # we need to update clockR and self.activeC because
         # the new_scheduleCZ.activeC are different from 
         copy.update_activeC(next_scheduleCZ.activeC)
            
         #raw_input("clockR: %s"%clockR)
         copy.reset(clockR) # step 1
         #raw_input('reset(%s): %s'%(clockR, copy))

         copy.slide(next_schedule)       # step 2 slide upto the upper bounds of each schedule 
         copy.tighten()                  # and then tighten it 
         #raw_input('slide(): %s'%(copy))

         #result = copy.intersect(next_scheduleCZ)
         #raw_input('intersect with(%s): %s'%(next_scheduleCZ, result))
         if TID.inf_trim_out:
            copy.activeC=set()
            for c in next_scheduleCZ.activeC:
               copy.activeC.add(c)
            copy.tighten() # 
            #raw_input('tighten: %s'%(result))

         return copy
      else:
         return None

   def successorOld(self, clockR, next_schedule):
      '''compute a TID (1) reseting self by clockR, (2) sliding it, and 
      (3) interseting with the TID constructed from ci=[t_s]
       Sliding(Resetting(varphi,clockR)) \cap Invariant(t_s)'''
      if isClockDict(next_schedule):
         next_scheduleCZ = TID()
         next_scheduleCZ.makeInvarient(next_schedule)

         copy = TID().copy(self)
         #raw_input('self: %s, copy(self): %s'%(self, copy))

         #if self != copy: # time consuming 
            #raise Exception("copy failed at %s"%function_name())

         #print 'next_scheduleCZ=', next_scheduleCZ

         #print 'newC=',
         #for c in next_schedule:
         #   print 'c=',str(next_schedule[c])

         #print 'newC=',next_scheduleCZ.activeC
         # we need to update clockR and self.activeC because
         # the new_scheduleCZ.activeC are different from 
         copy.update_activeC(next_scheduleCZ.activeC)
            
         #raw_input("clockR: %s"%clockR)
         copy.reset(clockR) # step 1
         #raw_input('reset(%s): %s'%(clockR, copy))

         copy.slide()       # step 2 slid forever
         #raw_input('slide(): %s'%(copy))

         result = copy.intersect(next_scheduleCZ)
         #raw_input('intersect with(%s): %s'%(next_scheduleCZ, result))
         if TID.inf_trim_out:
            result.activeC=set()
            for c in next_scheduleCZ.activeC:
               result.activeC.add(c)
            result.tighten() # 
            #raw_input('tighten: %s'%(result))

         return result
      else:
         return None

   @staticmethod
   def PrintRepository():
      print 'TID: |key_repo|=%d, |value_repo|=%d'%(len(TID.key_repo),len(TID.value_repo))

 
if __name__ == '__main__':
   a = TID().make({ ('c1',TID.c0): Interval(10,20), ('c2',TID.c0):Interval(5,8), 
                    ('c2','c1'): Interval(0,0) })
   print "a=", a
   b = TID().make({ ('c1',TID.c0): Interval(10,20), ('c2',TID.c0):Interval(5,7), 
                    ('c2','c1'): Interval(0,0) })
   print "b=", b
   print "a==b:", a==b, "a<b:", a < b, "a>b: ", a > b
